\begin{tabbing}
$\forall$\=$E$,$X_{1}$,$X_{2}$:Type, ${\it dE}$:EqDecider($E$), ${\it dL}$:EqDecider(IdLnk), ${\it info}$:($E$$\rightarrow$(\=(:Id $\times$ $X_{1}$) + (:(:IdLnk $\times$ $E$)\+\+
\\[0ex]$\times$ $X_{2}$))),
\-\\[0ex]$e$,$r$:$E$, $l$:IdLnk.
\-\\[0ex]($\uparrow$rcv{-}from{-}on(${\it dE}$; ${\it dL}$; ${\it info}$; $e$; $l$; $r$))
\\[0ex]$\Leftarrow\!\Rightarrow$ (($\uparrow$rcv?($r$)) c$\wedge$ ((sender($r$) = $e$) $\wedge$ (link($r$) = $l$)))
\end{tabbing}